We address the problem of formal and automated security verification of transport protocols for wireless sensor networks (WSN)\nthat may perform cryptographic operations. The verification of this class of protocols is difficult because they typically consist\nof complex behavioral characteristics, such as real-time, probabilistic, and cryptographic operations. To solve this problem, we\npropose a probabilistic timed calculus for cryptographic protocols and demonstrate how to use this formal language for proving\nsecurity or vulnerability of protocols. The main advantage of the proposed language is that it supports an expressive syntax and\nsemantics, allowing for studying real-time, probabilistic, and cryptographic issues at the same time. Hence, it can be used to verify\nsystems that involve these three properties in a convenient way. In addition, we propose an automatic verification method, based\non the well-known PAT process analysis toolkit, for this class of protocols. For demonstration purposes, we apply the proposed\nmanual and automatic proof methods for verifying the security of DTSN and SDTP, which are two of the recently proposedWSN\ntransport protocols.
Loading....